let f (x : int) where (x = 0)
= 1

deferred val eq_int : (int * int) -> bool
where (forall (x, y). post (eq_int) (x, y) (true) <=> x = y)
  and (forall (x, y). pre (eq_int) (x, y))

let { x } = if eq_int (x, 0) then f (x) else 0
